M, A:MsgA, k:Knd, y:Id, f:(A.stateA.da(k)ds(A)(y)?Void).
M.rframe(A.effect f of k on y)  Prop 

latex

Definitions	ds(M), M.rframe(A.effect f of k on y), M.state, M.da(a), (s1  s2 mod x), M.ds(x), 1of(t), MsgA, x:AB(x), State(ds), xdom(f). v=f(x)   P(x;v), x,y. t(x;y), P  Q, left+right, deq-member(eq;x;L), P  Q, A, Prop, s = t, f(a), {x:A| B(x) }, b, x  dom(f), a:A fp B(a), type List, x:AB(x), KindDeq, Top, f(x)?z, x. t(x), x:A. B(x), x.A(x), IdDeq, Type, Void, Id, t  T, Knd
Lemmas	Knd wf, Id wf, id-deq wf, fpf-cap wf, top wf, Kind-deq wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, not wf, deq-member wf, fpf-all wf, msga wf